M:MsgA, l:IdLnk. M sends on link l   

latex

Definitions	x:A. B(x), t  T, M sends on link l, t.2, t.1, x. t(x), MsgA, a:A fp B(a), Valtype(da;k), x(s)
Lemmas	IdLnk wf, msga wf, deq-member wf, idlnk-deq wf, map wf, Knd wf, pi2 wf